Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		concat(leaf,y)	→ y
2:		concat(cons(u,v),y)	→ cons(u,concat(v,y))
3:		less_leaves(x,leaf)	→ false
4:		less_leaves(leaf,cons(w,z))	→ true
5:		less_leaves(cons(u,v),cons(w,z))	→ less_leaves(concat(u,v),concat(w,z))

There are 4 dependency pairs:


6:		CONCAT(cons(u,v),y)	→ CONCAT(v,y)
7:		LESS_LEAVES(cons(u,v),cons(w,z))	→ LESS_LEAVES(concat(u,v),concat(w,z))
8:		LESS_LEAVES(cons(u,v),cons(w,z))	→ CONCAT(u,v)
9:		LESS_LEAVES(cons(u,v),cons(w,z))	→ CONCAT(w,z)

The approximated dependency graph contains 2 SCCs: {6} and {7}.

Consider the SCC {6}. There are no usable rules. By taking the AF π with π(CONCAT) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 6 is strictly decreasing.

Consider the SCC {7}. The usable rules are {1,2}. The constraints could not be solved.

Tyrolean Termination Tool (0.03 seconds) --- May 3, 2006